Termination Proof Script

• Consider the SCC {30}. There are no usable rules. By taking the AF π with π(ADD) = 1 together with the lexicographic path order with empty precedence, rule 30 is strictly decreasing.


• Consider the SCC {28}. There are no usable rules. By taking the AF π with π(DBL) = 1 together with the lexicographic path order with empty precedence, rule 28 is strictly decreasing.


• Consider the SCC {33}. There are no usable rules. By taking the AF π with π(HALF) = 1 together with the lexicographic path order with empty precedence, rule 33 is strictly decreasing.


• Consider the SCC {24}. There are no usable rules. By taking the AF π with π(SQR) = 1 together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.


• Consider the SCC {31,35,37-40}. The usable rules are {1-9,14-20}. By taking the AF π with π(activate) = π(ACTIVATE) = π(dbl) = π(n__s) = π(n__terms) = π(s) = π(sqr) = π(terms) = 1 and π(add) = π(cons) = π(FIRST) = 2 together with the lexicographic path order with precedence 0 ≻ nil and n__first ≈ first, the rules in {1-7,9,14-20,31,35,37} are weakly decreasing and the rules in {8,38-40} are strictly decreasing. There is one new SCC.
  • Consider the SCC {35,37}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__s) = 1 together with the lexicographic path order with empty precedence, rule 37 is weakly decreasing and rule 35 is strictly decreasing. There is one new SCC.
    • Consider the SCC {37}. By taking the AF π with π(ACTIVATE) = 1 together with the lexicographic path order with empty precedence, rule 37 is strictly decreasing.